Recent advances in computer and communication technologies have been promoting exchange of a large amount of information via public networks and dedicated networks in various industrial fields. Such communication often needs to exchange confidential information. Particularly in the fields of the financial industry, electronic commerce, etc., certification between operators, confidentiality of communication information and the like are required with a high accuracy. A variety of methods for ensuring the safety, such as cryptographic processing, have been developed and used. The safety of a provided service, when the strictness of cryptography is guaranteed, mainly depends on the safety of the cipher communication procedure used (for example, the certainty that “a secret key” used to decrypt the encrypted information is received only by an intended person). Therefore, verifying the safety of a developed cipher communication procedure is a very important technique for ensuring the secrecy of confidential information.
In the present application, “cipher communication procedure” includes data encryption and decryption procedures, and a procedure in which encrypted data are exchanged via communication lines, but does not include implementing methods such as the bit format of datagrams established by communications standards or the dynamic control of communication channels.
Moreover, “safety verification” denotes checking not only cipher communication procedure but also checking an operational procedure of a reactive system that receives external stimuli during operation and responds to-the stimuli repeatedly if it is described as intended. When the system will not be in any cases under unintended conditions, for example, dangerous conditions, the system is said to be “safe”. A system communicating encrypted information is also a type of reactive systems, cipher communication procedures can be regarded as an operational procedure of the system. In safety verification of cipher communication procedures, the electrical reliability and quality of actual communication lines are not included in the targets to be verified, and safety means the security of the information to be exchanged.
Heretofore, a method using a framework called regular tree automata based on automata theory as a verification method of cipher communication procedures is known. A verification method proposed early is disclosed in “Solving a Unification Problem under Constrained Substitutions Using Tree Automata” (Journal of Symbolic Computation 23(1), pp. 79-117, 1997) by Y. Kaji, T. Fujiwara and T. Kasami.
A method developed from the above-mentioned method is disclosed in “Abstracting Cryptographic Protocols with Tree Automata” (Proceeding of 6th International Static Analysis Symposium, Venice (Italy), Lecture Notes in Computer Science 1694, pp. 149-163, 1999) by David Monniaux, and “Rewriting for Cryptographic Protocol Verification” (Proceeding of 17th International Conference on Automated Deduction, Pittsburgh (Pa.), Lecture Notes in Computer Science 1831, pp. 271-290, 2000) by Thomas Genet and Francis Klay.
An automaton is a system that abstractly represents an actual device, system, etc. It can be in a plurality of states, and transition between the states occurs in response to “an input”. Possible states are not necessarily finite. When the automaton reached a predetermined final state from an initial state in response to one or a series of inputs INPUT, it is said that the INPUT is accepted by the automaton. In general, an automaton is written as (Σ, Q, Qf, Δ). Herein, Σ is a set of inputs (symbols), Q is a set of possible states, Qf is a set of final states, and Δ is a set of transition rules.
Therefore, if an automaton which accepts only the elements of a certain set and rejects the other can be given, processing of the set, i.e., processing of the elements of the set can be equivalently performed by using the automaton. This is particularly effective when the set to be processed consists of infinite elements.
A tree automaton represents an automaton which accepts data having a tree structure. Moreover, regular tree automaton represents a tree automaton which satisfies regular conditions.
When an cipher communication procedure, one of the targets to be verified, is represented by a formal language, it has been necessary to satisfy regular conditions. For this reason, approaches using known automata theories (formal language techniques) have been unsuccessful to automatically verify cipher communication procedures that do not satisfy regular conditions.
Although the verification methods suggested in the above-mentioned three theses can perform approximate security verification of cipher communication procedures that do not satisfy regular conditions, they are disadvantageously unable to perform strict verification.
This problem occurs not only to cipher communication procedures, but also to the operational procedures of common reactive systems.